Inference at * 
Iof proof for Lemma p-compose' wf:


  A, B, C:Type, g:(A(B + Top)), f:(ABC). f o' g  A(C + Top) 

latex

 by (Auto) 
CollapseTHEN ((Unfold `p-compose\'` ( 0)) 
CollapseTHEN (((if (((first_nat 2:n
C)) = 0) then (Repeat (MaAutoStep)) else (RepeatFor (first_nat 2:n) (MaAutoStep)))) 

C)CollapseTHEN ((Try ((Complete (Auto))))))) 

latex

C1: 

C1: 1. A : Type
C1: 2. B : Type
C1: 3. C : Type
C1: 4. g : A(B + Top)
C1: 5. ABC
C1: 6. x : A
C1: 7. (can-apply(g;x))
C1:   g(x)  (C + Top)
C.

Definitions	f o' g, x:A.B(x), Void, if b then t else f fi , can-apply(f;x), suptype(S; T), x.A(x), Type, Unit, P  Q, P & Q, x:A  B(x), , s = t, b, A, b, , inl x , do-apply(f;x), P  Q, f(a), left + right, Top, S  T, x:A. B(x), t  T, x:AB(x)
Lemmas	top wf, ifthenelse wf, can-apply wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, do-apply wf